http://www.isc.rit.edu/~icsa750/reading/ods.html

Why Protocol Description?

The ISO term is Formal Description Technique (FDT). A Formal Description is both a guide for implementors and it also allows dissemination of a protocol through
manufacturers. An Formal Description allows humans to reason about protocol. It simplifies the job of designing new protocols by providing a common framework for
the common parts of any protocol (this is analogous to using ALGOL type language to specify sequential algorithms). <#916#>#tex2html_wrap3870#<#916#> This
author finds formal methods genuinely useful. They are at their best when applied early in the design stage to capture the system behavior and enable analysis of
typical and boundary condition cases. They are at their least useful in communicating with a client. In the complex multilingual world of heterogeneous distributed
systems, they are a touchstone or <#826#> babel fish<#826#>. <#917#>#tex2html_wrap3872#<#917#> 

Why Protocol Specification?

In the short term, we can manually and semi-automatically check protocols. In the long term, we will be able to generate protocols from specifications in specialist
languages. We can <#829#> validate<#829#> a protocol - check that protocol is free from syntactic errors, and is simply self consistent. We can <#830#> verify<#830#>
protocol - can check that the protocol does actually provide the required functionality. 

     Free from deadlocks. States that it can't leave 
     Free from livelocks. States that conspire to lockout others. 
     Free from (useless) unreachable states. 
     Free from busy idle behavior. 
     May be able to analyze the performance of the protocol. 
     Can study event scheduling within protocol. 
     Can match event scheduling in network (other layers) to those in the protocol. 
     Can exploit genuine parallel nature of network components. 

Some Common Specification Systems

The first protocols were specified in a sort of structured English - text. This is very difficult to check for anything. Flowcharting has been used, but is an unnatural
framework for specifying concurrency, and leads to very large charts. It does, however allow for some automatic checking and generating of parts of a protocol. More
powerful techniques are: 

     State Diagrams - like Markov Diagrams. Very useful to humans, but get large and not machine readable. 
     Petri Nets A variety of state transition graphs, can help check protocols, but not intuitive for human implementor. 
     Grammers :- Backus Naur Form. Can be bent to describe formats and sequences of actions in a protocol, and is well known by programmers. Not so useful for
     checking for concurrency problems. 
     Format and Protocol languages. These are most promising for the future.